home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / pc_2.05.3 < prev    next >
Text File  |  1992-04-03  |  17KB  |  493 lines
  1. %%% PC prover
  2. %%% version 2.05.3 (based on pc_16.8)
  3. %%%   removed print_clause_list as it is also defined in auxiliary
  4. %%%   added support for Quintus Prolog
  5. %%%
  6. %%% Test of satisfiability based on the intelligent method.
  7. %%% intell_pc succeeds with flag of 'u' if the input set is unsatisfiable.
  8. %%% intell_pc succeeds with flag of 's' if the input set is satisfiable.
  9. %%% intell_pc can print out a model or relevant clauses.
  10. %%% The relevant clauses lists are maintained with delay merging technique.
  11. %%%
  12. %%% Three options are available:
  13. %%% tautology_rule: perform tautology deletion if it is set.
  14. %%% pure_literal_rule: perform pure literal deletion if it is set.
  15. %%% out_model_rc: print out model if the input is satisfiable.
  16. %%%               print out relevant clauses if the input is unsatisfiable.
  17. %%% Defaults are off.
  18. %%%
  19.  
  20.      pcprove(Clauses) :-
  21.     intell_pc(Clauses,Result),
  22.     !, Result == u.
  23.  
  24. %%% Update the accumulated pc time for statistics purpose.
  25.      update_pctime(TT3) :-
  26.     retract(pc_time(PCTIME)),
  27.     NEW_PCTIME is TT3 + PCTIME,
  28.     assert(pc_time(NEW_PCTIME)), !.
  29.      update_pctime(TT3) :-
  30.     assert(pc_time(TT3)), !.
  31.  
  32. %%% 1. clear database for pc prover only.
  33. %%% 2. transform clause into internal form.
  34. %%% 3. solve the problem.
  35. %%% 4. print out a minimum subset of unsatisfiable clauses.
  36.      intell_pc(S,R) :-
  37.     cputime(TT1),
  38.     intell_pc_prover(S,R),
  39.     cputime(TT2),
  40.     TT3 is TT2 -TT1,
  41.     update_pctime(TT3),
  42.     write_line(5,'PC prover(s): ',TT3), !.
  43.  
  44.      intell_pc_prover(S1,u) :-
  45.     clear_pc_database,
  46.     intell_pc_transform(S1,S2,PRS,Tag),
  47.     intell_pc_0(Tag,S2,PDS,PRS,[]),
  48.     pc_print_relevant_clauses(S1,PRS), !.
  49.      intell_pc_prover(_,s).
  50.  
  51.      clear_pc_database :- !.
  52.  
  53. %%% intell_pc_0 succeeds with dependent clause list if the input set 
  54. %%% is unsatisfiable.
  55. %%% intell_pc_0 fails with a model printed out if the input set 
  56. %%% is satisfiable.
  57.      intell_pc_0(Tag,_,_,_,_) :- Tag == unsat, !.
  58.      intell_pc_0(_,S1,PDS,PRS,PMS_In) :-
  59.     check_tautology_deletion(S1,S2),
  60.     !,
  61.     intell_pc_1(S2,PDS,PRS,PMS_In).
  62.  
  63. %%% If the input list is empty, then satisfiable.
  64. %%% Otherwise, call one literal deletion.
  65.      intell_pc_1([],_,_,PMS_In) :- pc_print_model(PMS_In), !, fail.
  66.      intell_pc_1(S1,PDS,PRS,PMS_In) :-
  67.     one_literal_deletion(S1,S2,Tag,PDS,PRS,PMS_In,PMS_M), 
  68.     !,
  69.     intell_pc_2(Tag,S2,PDS,PRS,PMS_M).
  70.  
  71. %%% If the input tag is unsat, return.
  72. %%% If the input list is empty, satisfiable.
  73. %%% Otherwise, go on.
  74.      intell_pc_2(Tag,_,_,_,_) :- Tag == unsat, !.
  75.      intell_pc_2(_,[],_,_,PMS_In) :- pc_print_model(PMS_In), !, fail.
  76.      intell_pc_2(_,S2,PDS,PRS,PMS_In) :-
  77.     intell_pc_2_1(S2,PDS,PRS,PMS_In).
  78.  
  79. %%% Check to execute pure literal deletion.
  80.      intell_pc_2_1(S1,PDS,PRS,PMS_In) :-
  81.     check_pure_literal_deletion(S1,S2),
  82.     !,
  83.     intell_pc_3(S2,PDS,PRS,PMS_In).
  84.  
  85. %%% If the input list is empty, satisfiable.
  86. %%% Otherwise, do case analysis.
  87.      intell_pc_3([],_,_,PMS_In) :- pc_print_model(PMS_In), !, fail.
  88.      intell_pc_3(S1,PDS,PRS,PMS_In) :-
  89.     !,
  90.     case_analysis(S1,PDS,PRS,PMS_In).
  91.  
  92. %%% Delete tautologies if tautology_rule is set.
  93.      check_tautology_deletion(S1,S2) :-
  94.     tautology_rule,
  95.     tautology_deletion(S1,S2), !.
  96.      check_tautology_deletion(S1,S1).
  97.  
  98.      tautology_deletion([prop(C1,_)|Cs1],S2) :-
  99.     tautology_clause(C1),
  100.     !,
  101.     tautology_deletion(Cs1,S2).
  102.      tautology_deletion([C1|Cs1],[C1|Cs2]) :-
  103.     !,
  104.     tautology_deletion(Cs1,Cs2).
  105.      tautology_deletion([],[]).
  106.  
  107. %%% Transform a clause into another data structure which contains
  108. %%% clause itself, and a pair of dependent lists for literals and
  109. %%% clauses.
  110. %%% If the input set has an empty clause, then Tag is set unsat
  111. %%% and PRS is the number of the empty clause.
  112.      intell_pc_transform(S1,S2,PRS,Tag) :-
  113.     intell_pc_transform(S1,1,S2,PRS,Tag), !.
  114.      intell_pc_transform([[]|_],N,_,[N],unsat) :- !.
  115.      intell_pc_transform([C|Cs],N,[prop(C,([],N))|Gs],PRS,Tag) :-
  116.     NN is N + 1,
  117.     !, intell_pc_transform(Cs,NN,Gs,PRS,Tag).
  118.      intell_pc_transform([],_,[],_,_).
  119.  
  120. %%% Suppose [Uc] is a unit clause. Delete all clauses containing Uc.
  121. %%% Delete all occurrences of not Uc from all clauses.
  122. %%% It is done recursively until all unit clauses are used.
  123.      one_literal_deletion(S1,S2,Tag,PDS,PRS,PMS_1,PMS_2) :-
  124.          one_literal_deletion(S1,S1,S2,Tag,PDS,PRS,PMS_1,PMS_2).
  125.      one_literal_deletion([prop([Uc],Upac)|Cs1],S1,S2,Tag,
  126.         PDS,PRS,PMS_1,PMS_2) :-
  127.     one_literal_deletion_round(Uc,Upac,S1,Sm,Tag,PDS,PRS),
  128.     !,
  129.     one_literal_deletion_1(Tag,Sm,S2,PDS,PRS,[Uc|PMS_1],PMS_2).
  130.      one_literal_deletion([_|Cs1],S1,S2,Tag,PDS,PRS,PMS_1,PMS_2) :-
  131.     !,
  132.     one_literal_deletion(Cs1,S1,S2,Tag,PDS,PRS,PMS_1,PMS_2).
  133.      one_literal_deletion([],S2,S2,_,_,_,PMS,PMS).
  134.  
  135.      one_literal_deletion_1(Tag,_,_,_,_,_,_) :- Tag == unsat, !.
  136.      one_literal_deletion_1(Tag,Sm,S2,PDS,PRS,PMS_1,PMS_2) :-
  137.     one_literal_deletion(Sm,Sm,S2,Tag,PDS,PRS,PMS_1,PMS_2).
  138.  
  139. %%% Pick one unit clause [Uc], and do one literal deletion on the
  140. %%% input set with Uc.
  141.      one_literal_deletion_round(Uc,Upac,S1,S2,Tag,PDS,PRS) :-
  142.     negate(Uc,NUc),
  143.     one_literal_deletion_round(Uc,NUc,Upac,S1,S2,Tag,PDS,PRS).
  144.      one_literal_deletion_round(Uc,NUc,Upac,[C1|Cs1],S2,Tag,PDS,PRS) :-
  145.     one_literal_deletion_clause(Uc,NUc,Upac,C1,S2,Sm,Tag,PDS,PRS),
  146.     !,
  147.     one_literal_deletion_round_1(Tag,Uc,NUc,Upac,Cs1,Sm,PDS,PRS).
  148.      one_literal_deletion_round(_,_,_,[],[],_,_,_).
  149.  
  150.      one_literal_deletion_round_1(Tag,_,_,_,_,_,_,_) :- Tag == unsat, !.
  151.      one_literal_deletion_round_1(Tag,Uc,NUc,Upac,Cs1,Sm,PDS,PRS) :-
  152.     one_literal_deletion_round(Uc,NUc,Upac,Cs1,Sm,Tag,PDS,PRS).
  153.  
  154. %%% Delete the underlying clauses if it is subsumed.
  155. %%% Update the underlying clause if it is simplified.
  156. %%% Pass the underlying clause if nothing happens.
  157.      one_literal_deletion_clause(Uc,NUc,Upac,prop(C1,Cpac),S2,Sm,Tag,PDS,PRS) :-
  158.     one_literal_deletion_clause_1(Uc,NUc,C1,C2,Res,_),
  159.     !,
  160.     one_literal_deletion_clause_2(C2,Res,Upac,Cpac,S2,Sm,Tag,PDS,PRS).
  161.      one_literal_deletion_clause(_,_,_,C1,[C1|Sm],Sm,_,_,_) :- !.
  162.  
  163. %%% Fails if nothing happens to the underlying clauses.
  164. %%% Return a flag of 'n' if the underlying clause is subsumed.
  165. %%% Return a variable flag if the underlying clause is simplified.
  166.      one_literal_deletion_clause_1(Uc,_,[Uc|_],d,n,_) :- !.
  167.      one_literal_deletion_clause_1(Uc,NUc,[NUc|Ls1],C2,Var1,s) :-
  168.     !,
  169.     one_literal_deletion_clause_1(Uc,NUc,Ls1,C2,Var1,s).
  170.      one_literal_deletion_clause_1(Uc,NUc,[L1|Ls1],[L1|Ls2],Var1,Var2) :-
  171.     !,
  172.          one_literal_deletion_clause_1(Uc,NUc,Ls1,Ls2,Var1,Var2).
  173.      one_literal_deletion_clause_1(_,_,[],[],_,n) :- !, fail.
  174.      one_literal_deletion_clause_1(_,_,[],[],_,_).
  175.  
  176. %%% Set Tag to be unsat if the simplified clause is empty.
  177. %%% Delete the underlying clauses if it is subsumed.
  178. %%% Update the underlying clause if it is simplified.
  179.      one_literal_deletion_clause_2([],_,(Utail,Nutail),(Ctail,Nctail),
  180.         _,_,unsat,PDS,PRS) :- 
  181.     merge(Utail,Ctail,PDS), 
  182.     check_pc_extract_numbers(Nutail,Nctail,PRS), !.
  183.      one_literal_deletion_clause_2(C2,s,(Utail,Nutail),(Ctail,Nctail),
  184.         [prop(C2,(Mtail,Mctail))|Sm],Sm,_,_,_) :-
  185.     merge(Utail,Ctail,Mtail), 
  186.     check_merge_expression(Nutail,Nctail,Mctail), !.
  187.      one_literal_deletion_clause_2(_,n,_,_,S2,S2,_,_,_) :- !.
  188.  
  189. %%% Perform pure literal deletion if pure_literal_rule is set.
  190.      check_pure_literal_deletion(S1,S2) :-
  191.     pure_literal_rule,
  192.     pure_literal_deletion(S1,S2), !.
  193.      check_pure_literal_deletion(S1,S1).
  194.  
  195. %%% Find pure literals first. 
  196. %%% Then delete all clauses containing one pure literal.
  197.      pure_literal_deletion(S1,S2) :-
  198.     find_pure_literals(S1,P1),
  199.     delete_pure_literals(P1,S1,S2).
  200.  
  201. %%% Find all distinct literals first.
  202. %%% Then decide which are pure literals.
  203.      find_pure_literals(S1,P1) :-
  204.     find_literals(S1,L1),
  205.     find_pure_literals_1(L1,P1).
  206.  
  207.      find_literals(S1,L1) :-
  208.     find_literals(S1,[],L1).
  209.      find_literals([prop(C,_)|Cs],A,L) :-
  210.     find_literals_clause(C,A,M),
  211.     !,
  212.     find_literals(Cs,M,L).
  213.      find_literals([],L,L).
  214.  
  215.      find_literals_clause([L|Ls],A,M) :-
  216.     member(L,A),
  217.     !,
  218.     find_literals_clause(Ls,A,M).
  219.      find_literals_clause([L|Ls],A,M) :-
  220.     !,
  221.     find_literals_clause(Ls,[L|A],M).
  222.      find_literals_clause([],M,M).
  223.  
  224. %%% Collect pure literals from the set of literals.
  225.      find_pure_literals_1([L|Ls],P) :-
  226.     not_pure_literal(L,Ls,Ls1),
  227.     !,
  228.     find_pure_literals_1(Ls1,P).
  229.      find_pure_literals_1([L|Ls],[L|P]) :-
  230.     !,
  231.     find_pure_literals_1(Ls,P).
  232.      find_pure_literals_1([],[]).
  233.  
  234. %%% A literal is pure if it is not a complement to the other literal.
  235.      not_pure_literal(L,Ls,Ls1) :-
  236.     negate(L,NL),
  237.     !,
  238.     delete_and_rest(NL,Ls,Ls1).
  239.  
  240. %%% Succeeds with the list with NL deleted.
  241. %%% Fails if NL is not a member of the input list.
  242.      delete_and_rest(NL,[NL|Ls],Ls) :- !.
  243.      delete_and_rest(NL,[L|Ls],[L|Ls1]) :-
  244.          !, delete_and_rest(NL,Ls,Ls1).
  245.  
  246. %%% Delete any clause containg one pure literal.
  247. %%% Pick one pure literal L, delete any clause containing L.
  248. %%% Then pick the next literal. Do iteratively until empty set.
  249.      delete_pure_literals([L|Ls],S1,S2) :-
  250.     delete_pure_literal(L,S1,Sm),
  251.     !,
  252.     delete_pure_literals(Ls,Sm,S2).
  253.      delete_pure_literals([],S2,S2).
  254.  
  255. %%% Delete any clause containing L.
  256.      delete_pure_literal(L,[prop(C1,_)|Cs1],Sm) :-
  257.     member(L,C1),
  258.     !,
  259.     delete_pure_literal(L,Cs1,Sm).
  260.      delete_pure_literal(L,[C1|Cs1],[C1|Sm]) :-
  261.     !,
  262.     delete_pure_literal(L,Cs1,Sm).
  263.      delete_pure_literal(_,[],[]).
  264.  
  265. %%% Pick a literal from the shortest negative clause and perform
  266. %%% case analysis if both positive and negative clauses exist. 
  267. %%% Otherwise print out model if requested and fails.
  268.      case_analysis(S1,PDS,PRS,PMS_In) :-
  269.     case_clause(S1,C1),
  270.     C1 = [L1|_],
  271.     negate(L1,NL1),
  272.     !,
  273.     affirmative_case(L1,NL1,S1,PDSa,PRSa,[L1|PMS_In]),
  274.     !,
  275.     check_negative_case(L1,NL1,PDSa,PRSa,S1,PDS,PRS,[NL1|PMS_In]).
  276.      case_analysis(S1,_,_,PMS_In) :-
  277.     out_model_rc,
  278.         find_model_clauses(S1,M1),
  279.         append(PMS_In,M1,M2),
  280.         pc_print_model_1(M2),
  281.     !, fail.
  282.  
  283.      find_model_clauses([prop(List,_)|Cs1],[L|Ms]) :-
  284.     member(L,List),
  285.         negate(L,NL), 
  286.         reduce_set(L,NL,Cs1,Cs2,Tag,_,_),   
  287.     Tag \== unsat,
  288.         !, find_model_clauses(Cs2,Ms).    
  289.      find_model_clauses([],[]).
  290.  
  291. %%% Find a clause for case analysis.
  292.      case_clause(S1,C1) :-
  293.     pn_clauseset(S1,C1).
  294.  
  295. %%% pn_clauseset succeeds with the first smallest negative clause
  296. %%% if both positive and negative clauses exist.
  297.      pn_clauseset([prop(C,_)|Gs],Nc) :-
  298.     pn_clause(C,Var),!,
  299.     porn_clauseset(Var,Gs,C,Nc).
  300.      pn_clauseset([_|Gs],Nc) :-
  301.     !, pn_clauseset(Gs,Nc).
  302.  
  303. %%% Succeeds if both positive and negative clauses are found.
  304.      porn_clauseset(n,Gs,C,Nc) :-
  305.     length(C,L), !,
  306.     p_clauseset(Gs,C,L,Nc), !.
  307.      porn_clauseset(p,Gs,_,Nc) :-
  308.     n_clauseset(Gs,Nc).
  309.     
  310. %%% Succeeds if a positive clause exists.
  311. %%% At the same time, find the first smallest negative clause.
  312.      p_clauseset([prop(C2,_)|Gs],C1,L1,Nc) :-
  313.     pn_clause(C2,Var), !,
  314.     p_clauseset_1(Var,Gs,C1,L1,C2,Nc), !.
  315.      p_clauseset([_|Gs],C1,L1,Nc) :-
  316.     !, p_clauseset(Gs,C1,L1,Nc).
  317.  
  318.      p_clauseset_1(n,Gs,C1,2,_,Nc) :-
  319.     !,
  320.     p_clauseset(Gs,C1,2,Nc).
  321.      p_clauseset_1(n,Gs,C1,L1,C2,Nc) :-
  322.     length(C2,L2),
  323.     shorter_clause(C2,L2,C1,L1,C3,L3),
  324.     !,
  325.     p_clauseset(Gs,C3,L3,Nc).
  326.      p_clauseset_1(p,_,C1,2,_,C1) :- !.
  327.      p_clauseset_1(p,Gs,C1,L1,_,Nc) :-
  328.     shortest_negative_clause(Gs,C1,L1,Nc).
  329.  
  330. %%% Find the first smallest negative clause.
  331.      shortest_negative_clause([prop(C2,_)|Gs],C1,L1,Nc) :-
  332.     negclause(C2),
  333.     length(C2,L2),
  334.     shortest_negative_clause_1(L2,Gs,C1,L1,C2,Nc), !.
  335.      shortest_negative_clause([_|Gs],C1,L1,Nc) :-
  336.     !,
  337.     shortest_negative_clause(Gs,C1,L1,Nc).
  338.      shortest_negative_clause([],Nc,_,Nc).
  339.  
  340.      shortest_negative_clause_1(2,_,_,_,C2,C2) :- !.
  341.      shortest_negative_clause_1(L2,Gs,C1,L1,C2,Nc) :-
  342.     shorter_clause(C2,L2,C1,L1,C3,L3),
  343.     shortest_negative_clause(Gs,C3,L3,Nc).
  344.  
  345. %%% Succeeds with the first smallest negative clause.
  346.      n_clauseset([prop(C1,_)|Gs],Nc) :-
  347.     pn_clause(C1,Var),
  348.     !,
  349.     n_clauseset_1(Var,Gs,C1,Nc), !.
  350.      n_clauseset([_|Gs],Nc) :-
  351.     !, n_clauseset(Gs,Nc).
  352.  
  353.      n_clauseset_1(n,Gs,C1,Nc) :-
  354.     length(C1,L1),
  355.     n_clauseset_1_1(L1,Gs,C1,Nc), !.
  356.      n_clauseset_1(p,Gs,_,Nc) :-
  357.     !,
  358.     n_clauseset(Gs,Nc).
  359.  
  360.      n_clauseset_1_1(2,_,C1,C1) :- !.
  361.      n_clauseset_1_1(L1,Gs,C1,Nc) :-
  362.     shortest_negative_clause(Gs,C1,L1,Nc).
  363.  
  364.      shorter_clause(C1,L1,_,L2,C1,L1) :-
  365.     L1 < L2, !.
  366.      shorter_clause(_,_,C2,L2,C2,L2).
  367.  
  368. %%% Perform affirmative case.
  369.      affirmative_case(L1,NL1,S1,PDSa,PRSa,PMS_In) :- 
  370.     test_set(L1,NL1,S1,PDSa,PRSa,PMS_In).
  371.  
  372. %%% Perform negative case if the affirmative case depends on
  373. %%% affirmative assumption.
  374. %%% Otherwise, don't perform negative case and the dependent lists 
  375. %%% are those of affirmative case.
  376.      check_negative_case(L1,NL1,PDSa,PRSa,S1,PDS,PRS,PMS_In) :-
  377.     delete_and_rest(L1,PDSa,PDSaa),
  378.     !,
  379.     negative_case(L1,NL1,S1,PDSn,PRSn,PMS_In),
  380.     dependency_expansion(PDSaa,PRSa,NL1,PDSn,PRSn,PDS,PRS), !.
  381.      check_negative_case(_,_,PDSa,PRSa,_,PDSa,PRSa,_).
  382.  
  383. %%% Perform negative case.
  384.      negative_case(L1,NL1,S1,PDSn,PRSn,PMS_In) :-
  385.     test_set(NL1,L1,S1,PDSn,PRSn,PMS_In).
  386.  
  387. %%% The dependent lists are the union of dependent lists of
  388. %%% affirmative case and negative case if the negative case 
  389. %%% depends on the negative assumption.
  390. %%% Otherwise, the dependent lists are those of negative case.
  391.      dependency_expansion(PDSaa,PRSa,NL1,PDSn,PRSn,PDS,PRS) :-
  392.     delete_and_rest(NL1,PDSn,PDSnn),
  393.     merge(PDSaa,PDSnn,PDS), 
  394.     check_ordered_merge(PRSa,PRSn,PRS), !.
  395.      dependency_expansion(_,_,_,PDSn,PRSn,PDSn,PRSn).
  396.  
  397.      test_set(L1,NL1,S1,PDS,PRS,PMS_In) :-
  398.     reduce_set(L1,NL1,S1,S2,Tag,PDS,PRS),
  399.     !,
  400.     test_set_1(Tag,S2,PDS,PRS,PMS_In).
  401.  
  402.      test_set_1(Tag,_,_,_,_) :- Tag == unsat, !.
  403.      test_set_1(_,S1,PDS,PRS,PMS_In) :-
  404.     intell_pc_1(S1,PDS,PRS,PMS_In).
  405.  
  406. %%% Perform reduction with assumption L.
  407.      reduce_set(L,NL,[prop(C1,Cpac)|Cs1],S2,Tag,PDS,PRS) :-
  408.     reduce_clause(L,NL,C1,C2,Var1),
  409.     !,
  410.     reduce_set_1(C2,Var1,Cpac,L,NL,Cs1,S2,Tag,PDS,PRS).
  411.      reduce_set(L,NL,[C1|Cs1],[C1|Cs2],Tag,PDS,PRS) :-
  412.     !,
  413.     reduce_set(L,NL,Cs1,Cs2,Tag,PDS,PRS).
  414.      reduce_set(_,_,[],[],_,_,_).
  415.  
  416.      reduce_set_1([],_,(Ctail,Nctail),L,_,_,_,unsat,[L|Ctail],Nctail) :- !.
  417.      reduce_set_1(C2,s,(Ctail,Nctail),L,NL,Cs1,
  418.         [prop(C2,([L|Ctail],Nctail))|Cs2],Tag,PDS,PRS) :-
  419.     reduce_set(L,NL,Cs1,Cs2,Tag,PDS,PRS), !.
  420.      reduce_set_1(_,n,_,L,NL,Cs1,S2,Tag,PDS,PRS) :-
  421.     reduce_set(L,NL,Cs1,S2,Tag,PDS,PRS).
  422.  
  423. %%% Fails if nothing happens to the underlying clause.
  424. %%% Succeeds with flag of 'n' if the underlying clause is subsumed.
  425. %%% Succeeds with variable flag if the underlying clause is simplified.
  426.      reduce_clause(L,NL,C1,C2,Var1) :-
  427.          reduce_clause(L,NL,C1,C2,Var1,Var2).
  428.      reduce_clause(L,_,[L|_],-1,n,_) :- !.
  429.      reduce_clause(L,NL,[NL|Ls1],C2,Var1,s) :-
  430.     !, reduce_clause(L,NL,Ls1,C2,Var1,s).
  431.      reduce_clause(L,NL,[L1|Ls1],[L1|Ls2],Var1,Var2) :-
  432.     !, reduce_clause(L,NL,Ls1,Ls2,Var1,Var2).
  433.      reduce_clause(_,_,[],[],_,n) :- !, fail.
  434.      reduce_clause(_,_,[],[],_,_).
  435.  
  436. %%% print out literals in PMS_In.
  437.      pc_print_model(PMS_In) :-
  438.     out_model_rc,
  439.     pc_print_model_1(PMS_In), !.
  440.      pc_print_model(_).
  441.  
  442.      pc_print_model_1(PMS_In) :-
  443.     write_line(5,'Model:'),
  444.     print_clause_list(PMS_In), !.
  445.  
  446. %%% don't care about relevant clauses list if out_model_rc is not asserted.
  447.      check_pc_extract_numbers(Nutail,Nctail,PRS) :-
  448.     out_model_rc,
  449.     pc_extract_numbers(mr(Nutail,Nctail,X1),PRS), !.
  450.      check_pc_extract_numbers(_,_,_).
  451.  
  452. %%% don't care about relevant clauses list if out_model_rc is not asserted.
  453.      check_merge_expression(Nutail,Nctail,Mctail) :-
  454.     out_model_rc,
  455.     Mctail = mr(Nutail,Nctail,X1), !.
  456.      check_merge_expression(_,_,_).
  457.  
  458. %%% don't care about relevant clauses list if out_model_rc is not asserted.
  459.      check_ordered_merge(PRSa,PRSn,PRS) :-
  460.     out_model_rc,
  461.     ordered_merge(PRSa,PRSn,PRS), !.
  462.      check_ordered_merge(_,_,_).
  463.  
  464. %%% extract the clause numbers and print out them.
  465.      pc_print_relevant_clauses(S1,Z2) :-
  466.     out_model_rc,
  467.     write_line(5,'PC relevant clauses:'),
  468.     print_ordered_clauses(Z2,S1), !.
  469.      pc_print_relevant_clauses(_,_).
  470.  
  471.      pc_extract_numbers(mr(X,Y,Z),Z) :-
  472.     nonvar(Z), !.
  473.      pc_extract_numbers(mr(X,Y,Z),Z) :-
  474.     pc_extract_numbers(X,Z1),
  475.     pc_extract_numbers(Y,Z2),
  476.     ordered_merge(Z1,Z2,Z), !.
  477.      pc_extract_numbers(X,[X]).
  478.  
  479. %%% Print out clauses in order specified in a list.
  480.      print_ordered_clauses(N2,S1) :-
  481.     print_ordered_clauses(N2,1,S1).
  482.      print_ordered_clauses([N|Ns],N,[C|Cs]) :-
  483.     write_numberedline_head(10,N,'.'),
  484.     write_line(2,C),
  485.     NN is N + 1,
  486.     !,
  487.     print_ordered_clauses(Ns,NN,Cs).
  488.      print_ordered_clauses(Ns,N,[C|Cs]) :-
  489.     NN is N + 1,
  490.     !,
  491.     print_ordered_clauses(Ns,NN,Cs).
  492.      print_ordered_clauses([],_,_).
  493.